Adding package management infrastructure by rlepigre-skylabs-ai · Pull Request #21564 · rocq-prover/rocq

rlepigre-skylabs-ai · 2026-01-29T21:12:08Z

This PR implement rocq-prover/rfcs#101, whose goal is to add a proper notion of Rocq package (piggy-backing on findlib), setting a path towards the eventual removal of the infamous coq/user-contrib directory. This was discussed in a Rocq Call.

Summary of the changes

Rocq CLI tools (rocq c, rocq dep, ...) now accept a -package <pkg> argument (similar to that of ocamlfind).
A rocq find command was added to list installed packages (directory and Rocq module path), and allowing to obtain the necessary -Q / -I flags for a given list of packages (or all of them).
The Corelib and Ltac2 libraries are installed twice: once under coq/user-contrib for backwards compatibility, and once as Rocq packages.
The rocq makefile command now takes a --rocq-package <pkgname> argument which can be used to request the use of the new package infrastructure (not using it is deprecated), together with dependencies specified via -package. A --legacy-support flag can be used to also install under coq/user-contrib.

Testing done

Correct Rocq install

Checked that Rocq installs correctly with the new installation scheme, including Rocq packages rocq-core and rocq-core.ltac2 that can be requested as packages.

Correct `rocq-stdlib` install

Checked that the Rocq standard library can be ported to the new system (via rocq makefile), and installs correctly after applying the following changes.

diff --git a/.gitignore b/.gitignore
index a93e1261a9..e0410c6a3d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -164,3 +164,4 @@ user-contrib/Ltac2/dune
 .wrappers
 doc/stdlib/Library.fdb_latexmk
 doc/stdlib/Library.fls
+theories/META.*
diff --git a/theories/_CoqProject b/theories/_CoqProject
index b34d8dd88a..cc961853c7 100644
--- a/theories/_CoqProject
+++ b/theories/_CoqProject
@@ -1,3 +1,7 @@
+--rocq-package rocq-stdlib
+-package rocq-core
+--legacy-support
+--description "Rocq standard library"
 -R . Stdlib
 # When editing below lines, keep the theories/dune file in sync
 # to handle when requiring Rocq >= 9.2

Correct `bignums` install

Checked that a simple plugin (bignums) builds and install correctly using rocq makefile after the following changes.

diff --git a/Makefile b/Makefile
index 1da733b..c3b27b6 100644
--- a/Makefile
+++ b/Makefile
@@ -8,7 +8,8 @@ clean: Makefile.coq
 _CoqProject:;

 Makefile.coq: _CoqProject
-       $(COQBIN)rocq makefile -f _CoqProject -o Makefile.coq
+       $(COQBIN)rocq makefile -f _CoqProject -o Makefile.coq \
+               --rocq-package coq-bignums --legacy-support -package rocq-stdlib

 %: Makefile.coq
        $(MAKE) -f Makefile.coq $@

Ensured that this can work with dune

Opened a dune PR that enables using the new installation scheme from dune projects. This dune version was tested using ports of equations, rocq-stdpp, and rocq-iris. And also a composed build of the latter two.

rlepigre-skylabs-ai · 2026-01-29T21:22:57Z

Regarding the adaptation of rocq makefile, I believe that we wouldn't even need the -package options to the various commands, and that rocqfind would be sufficient for compilation (provided that install packages follow the expected installation scheme). All we'd need to do is ask the user to give a list of package dependencies in a variable ROCQ_PACKAGES, and then we could do something like the following in the generated Makefile:

DEPS_ARGS := $(shell rocqfind -Q -I ${ROCQ_PACKAGES} | tr '\n' ' ')

We would then add ${DEPS_ARGS} to all invoked rocq commands, in addition to the -Q / -R / -I that are needed for the local plugins / theories, and things would just work.

Of course, we'd still need to make sure that make install respects the installation scheme.

SkySkimmer · 2026-01-30T14:11:01Z

the -I argument and output of rocqfind seems wrong: -I dir as an argument of rocqdep / rocqc means "add dir to OCAMLPATH". Since rocqfind gets its info from OCAMLPATH it has nothing new to add. The output it gives is also wrong since it prints directories which don't lead to META files. Finally when the _CoqProject contains -I dir (because there is a local META in dir) it seems like rocqfind should be informed about it.
I don't understand the point of rocqfind, shouldn't rocqc/rocqdep understand -package directly? also what is the point of the cmxs output

rlepigre-skylabs-ai · 2026-01-30T14:53:58Z

the -I argument and output of rocqfind seems wrong: -I dir as an argument of rocqdep / rocqc means "add dir to OCAMLPATH". Since rocqfind gets its info from OCAMLPATH it has nothing new to add. The output it gives is also wrong since it prints directories which don't lead to META files.

Good point, I now only add -I for the directories containing the META file.

Finally when the _CoqProject contains -I dir (because there is a local META in dir) it seems like rocqfind should be informed about it.

Yeah, maybe. I was thinking of rocqfind as a way of looking up actually installed stuff, not something we'd use for local plugins for example. I also don't know if rocqfind is useful in itself, but I thought it could be useful for rocq makefile-generated Makefiles.

I don't understand the point of rocqfind, shouldn't rocqc/rocqdep understand -package directly? also what is the point of the cmxs output

Yeah, I think they probably should, yes.

I initially thought of the cmxs output as a way to get external dependencies, for example in Makefile rules, to get sounder builds when they change. However that's probably not necessary, because the .vo has the hash of the .cmxs it directly uses, right?

rlepigre-skylabs-ai · 2026-01-30T14:55:10Z

Regarding adding a -package option to rocq c, what do you think is the best way to do that? I see there are several places in the code base where argument parsing is done, and I was hoping not to duplicate the code everywhere (rocq doc, rocqchk, ...).

SkySkimmer · 2026-01-30T14:55:31Z

the .vo has the has of the .cmxs it directly uses, right?

if "has the has" is meant to be "contains the hash" then yes

rlepigre-skylabs-ai · 2026-01-30T14:56:39Z

if "has the has" is meant to be "contains the hash" then yes

Oups, I edited the comment.

rlepigre-skylabs-ai · 2026-02-02T18:10:32Z

I've now added the -package option in all places where I could find a -Q option being supported.

rlepigre-skylabs-ai · 2026-02-04T23:13:59Z

@SkySkimmer what do you think should be the next steps here? Should I make it so that Corelib and Ltac2 get installed as packages (in addition to the current installation scheme)?

It's also not clear to me how to make tests for this PR. Any recommendation on that front?

SkySkimmer · 2026-02-05T12:45:37Z

I still don't understand what the transition is supposed to look like.
Are we supposed to install copies of packages in user-contrib and in their own lib/ subdir? That sounds like a waste of disk space.

rlepigre-skylabs-ai · 2026-02-05T12:50:50Z

That seems like the easiest thing to do (potentially using symbolic links instead of actual copies, but that might lead to problems). Do you see another alternative?

SkySkimmer · 2026-02-05T12:54:06Z

I don't think the argument parsing in coqproject_file and coqargs are the right places to call resolve. Is findlib even initialized when we're in that code?

It's also not clear to me how to make tests for this PR. Any recommendation on that front?

test-suite/coq-makefile and test-suite/misc have tests which are arbitrary scripts

That seems like the easiest thing to do (potentially using symbolic links instead of actual copies, but that might lead to problems). Do you see another alternative?

If we have copies (including symbolic links) won't they get detected as conflicts? eg Require Prelude would say "found prelude.vo in lib/coq/theories/... and lib/rocq-core/..."

rlepigre-skylabs-ai · 2026-02-05T13:10:32Z

That seems like the easiest thing to do (potentially using symbolic links instead of actual copies, but that might lead to problems). Do you see another alternative?

If we have copies (including symbolic links) won't they get detected as conflicts? eg Require Prelude would say "found prelude.vo in lib/coq/theories/... and lib/rocq-core/..."

I guess that any particular project you should not rely both on packages and on lib/coq/user-contrib and lib/coq/theories. Either the package is ported, and only uses packages (and transitively for its deps), or it uses a legacy mode that does not allow packages.

Do you think something like that could work?

SkySkimmer · 2026-02-05T13:34:10Z

Do we really want to force the transition order like that?

rlepigre-skylabs-ai · 2026-02-05T13:37:33Z

I think this would be OK if package that have transitioned can be depended on by packages that have not, which would simply mean double-installing everything.

To me, it seems fine to require that a package can only transition if all its dependencies have.

SkySkimmer · 2026-02-05T13:40:14Z

also isn't part of the point of this system that we can multiple packages using the same logical paths? but such packages can't be double installed

rlepigre-skylabs-ai · 2026-02-05T13:41:26Z

Yeah, that's a good point. I guess they can't right now, so at least that's not a regression. We can only get that benefit when the legacy installation method is removed I guess.

SkySkimmer · 2026-02-05T13:48:37Z

If we installed only once, we could have coqdep/coqc implicitly add -Q for all findlib packages if no -package is used.
Then a project must give either all or none of its dependencies with -package.
Installed conflicting packages would only error (ambiguous require) if attempted to be used without -package.

This may break dune though.

SkySkimmer · 2026-07-08T13:49:00Z

@coqbot run full ci

SkySkimmer

should be ready AFAICT assuming CI doesn't suddenly break

rlepigre-skylabs-ai · 2026-07-08T14:14:20Z

@coqbot run full ci

rlepigre-skylabs-ai · 2026-07-08T14:15:28Z

should be ready AFAICT assuming CI doesn't suddenly break

Sorry, I had not seen this message when I last pushed. I have extended the docs with explanations of the new installation layout.

SkySkimmer · 2026-07-08T14:59:17Z

+They can be combined::
+
+   $ rocq find -Q -I my-package
+   -Q '/path/to/lib/my-package/rocq.d' MyPackage


what's the quoting here? (ocaml, shell, other?)

It's using Filename.quote, whose documentation starts with the following.

Return a quoted version of a file name, suitable for use as one argument in a command line, escaping all meta-characters.

SkySkimmer · 2026-07-08T20:13:32Z

@coqbot merge now

Fixing an unfortunate variable overlap from rocq-prover#21564

Fixing an unfortunate variable overlap from #21564 (cherry picked from commit e964f5c)

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jan 29, 2026

rlepigre-skylabs-ai force-pushed the package branch from 6fd2b26 to fd3edd8 Compare January 29, 2026 21:38

rlepigre-skylabs-ai force-pushed the package branch from fd3edd8 to 5f9a342 Compare January 30, 2026 14:47

rlepigre-skylabs-ai force-pushed the package branch from 5f9a342 to 0fd9ef3 Compare February 2, 2026 18:08

rlepigre-skylabs-ai force-pushed the package branch from 0fd9ef3 to 52646c6 Compare February 2, 2026 22:37

rlepigre-skylabs-ai mentioned this pull request Feb 3, 2026

Coq/Rocq support still uses hard-coded coq/user-contrib ocaml/dune#13532

Open

rlepigre-skylabs-ai force-pushed the package branch from 52646c6 to 9a4ae80 Compare April 9, 2026 15:45

rlepigre-skylabs-ai marked this pull request as ready for review April 9, 2026 16:26

rlepigre-skylabs-ai requested review from a team as code owners April 9, 2026 16:26

rlepigre-skylabs-ai added 9 commits July 8, 2026 15:44

Add -package option to [rocq doc].

b048705

Add -package option to [rocqnative].

8131307

Also install Corelib / ltac2 with the new scheme.

76dbd18

Add [rocq makefile] support for installing packages.

f7f9f19

Add changelog entry.

fb93366

Apply suggestions.

1934c83

More documentation.

9346d07

Remove dummy version info from generated META.

f105c60

Add [rocq find] test.

08960a6

rlepigre-skylabs-ai force-pushed the package branch from f3bc9b2 to 08960a6 Compare July 8, 2026 13:44

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 8, 2026

SkySkimmer approved these changes Jul 8, 2026

View reviewed changes

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 8, 2026

More complete docs.

d7e43b7

rlepigre-skylabs-ai force-pushed the package branch from 8502188 to d7e43b7 Compare July 8, 2026 14:13

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 8, 2026

SkySkimmer reviewed Jul 8, 2026

View reviewed changes

SkySkimmer added this to the 9.3+rc1 milestone Jul 8, 2026

coqbot-app Bot merged commit d77b754 into rocq-prover:master Jul 8, 2026
8 of 9 checks passed

proux01 reviewed Jul 9, 2026

View reviewed changes

Comment thread tools/CoqMakefile.in

proux01 mentioned this pull request Jul 9, 2026

[rocq makefile] Don't erase ROCQPATH #22246

Merged

proux01 added a commit to proux01/rocq that referenced this pull request Jul 9, 2026

[rocq makefile] Don't erase ROCQPATH

c1c8628

Fixing an unfortunate variable overlap from rocq-prover#21564

proux01 added a commit to proux01/rocq that referenced this pull request Jul 9, 2026

[rocq makefile] Don't erase ROCQPATH

e964f5c

Fixing an unfortunate variable overlap from rocq-prover#21564

rlepigre-skylabs-ai mentioned this pull request Jul 9, 2026

Share flags config by generating _CoqProject rocq-prover/stdlib#285

Closed

SkySkimmer mentioned this pull request Jul 10, 2026

support for -package ProofGeneral/PG#878

Open

gares pushed a commit that referenced this pull request Jul 22, 2026

[rocq makefile] Don't erase ROCQPATH

30d810b

Fixing an unfortunate variable overlap from #21564 (cherry picked from commit e964f5c)

Uh oh!

Conversation

rlepigre-skylabs-ai commented Jan 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary of the changes

Testing done

Correct Rocq install

Correct rocq-stdlib install

Correct bignums install

Ensured that this can work with dune

Uh oh!

rlepigre-skylabs-ai commented Jan 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SkySkimmer commented Jan 30, 2026

Uh oh!

rlepigre-skylabs-ai commented Jan 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

rlepigre-skylabs-ai commented Jan 30, 2026

Uh oh!

SkySkimmer commented Jan 30, 2026

Uh oh!

rlepigre-skylabs-ai commented Jan 30, 2026

Uh oh!

rlepigre-skylabs-ai commented Feb 2, 2026

Uh oh!

rlepigre-skylabs-ai commented Feb 4, 2026

Uh oh!

SkySkimmer commented Feb 5, 2026

Uh oh!

rlepigre-skylabs-ai commented Feb 5, 2026

Uh oh!

SkySkimmer commented Feb 5, 2026

Uh oh!

rlepigre-skylabs-ai commented Feb 5, 2026

Uh oh!

SkySkimmer commented Feb 5, 2026

Uh oh!

rlepigre-skylabs-ai commented Feb 5, 2026

Uh oh!

SkySkimmer commented Feb 5, 2026

Uh oh!

rlepigre-skylabs-ai commented Feb 5, 2026

Uh oh!

SkySkimmer commented Feb 5, 2026

Uh oh!

SkySkimmer commented Jul 8, 2026

Uh oh!

SkySkimmer left a comment

Choose a reason for hiding this comment

Uh oh!

rlepigre-skylabs-ai commented Jul 8, 2026

Uh oh!

rlepigre-skylabs-ai commented Jul 8, 2026

Uh oh!

SkySkimmer Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

rlepigre-skylabs-ai Jul 8, 2026

Choose a reason for hiding this comment

Uh oh!

SkySkimmer commented Jul 8, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

rlepigre-skylabs-ai commented Jan 29, 2026 •

edited

Loading

Correct `rocq-stdlib` install

Correct `bignums` install

rlepigre-skylabs-ai commented Jan 29, 2026 •

edited

Loading

rlepigre-skylabs-ai commented Jan 30, 2026 •

edited

Loading